Théorème de Rabin sur les arbres
En informatique théorique, le théorème de Rabin sur les arbres énonce la décidabilité de la théorie monadique du second ordre de l'arbre binaire infini complet, mais aussi des arbres infinis d'arité finie fixée, et de l'arbre infini d'arité dénombrable. Ce théorème a été démontré par Michael Rabin en 1969[1],[2].
Démonstrations[modifier | modifier le code]
Il existe plusieurs démonstrations de ce théorème dans la littérature[réf. nécessaire]. L'article original de Rabin utilise des automates d'arbres non déterministes avec des conditions dites de Rabin[1].
Applications[modifier | modifier le code]
Le théorème de Rabin sur les arbres permet de démontrer que[2] :
- la logique modale S4 est décidable ;
- la logique modale KvB est décidable ;
- la théorie monadique des ordres linéaires dénombrables est décidable;
- la logique du mu-calcul, la logique temporelle CTL* sont décidables.
Notes et références[modifier | modifier le code]
- (en) Michael O. Rabin, « Decidability of second-order theories and automata on infinite trees », Bull. Amer. Math. Soc., vol. 74, no 5, , p. 1025-1029 (lire en ligne, consulté le )
- (en) S. Steinert-Threlkeld, « Rabin's Tree Theorem and Applications », .
